;;;(INST E PAT ML) is an a-list that will yield E when substituted in PAT.
;;;ML is an a-list of privioulsy committed substitutions, usually NIL to begin.
;;;INST requires a predicate ISVAR to identify variables.


;;;the pattern matcher. ML is the list of variable bindings necessary to make 
;;;   PAT match E.
(DEFUN INST (E PAT ML) 
  (COND ((EQ ML (QUOTE NO)) ML) 
	((ATOM PAT) (COND ((ISVAR PAT)
		         ((LAMBDA (W) (COND ((NULL W) (CONS (CONS PAT E) ML))
					    ((EQUAL (CDR W) E) ML) 
					    (T (QUOTE NO)))) 
  			  (ASSOC PAT ML)))
			 ((EQ PAT E) ML) 
			 (T (QUOTE NO)))) 
	((ATOM E) (QUOTE NO))
	(T (INST (CDR E) (CDR PAT) (INST (CAR E) (CAR PAT) ML)))))

(DEFUN ISVAR (M) (MEMBER M (QUOTE (U V W X Y Z))))

;;;This sublis creates no unnecessary list structure.

(DEFUN SUBLIS (L E) 
  (COND ((ATOM E) 
         ((LAMBDA (W) (COND ((NULL W) E) (T (CDR W)))) (ASSOC E L)))
	(T ((LAMBDA (X Y) 
	      (COND ((AND (EQ X (CAR E))(EQ Y (CDR E))) E) (T (CONS X Y)))) 
	    (SUBLIS L (CAR E)) (SUBLIS L (CDR E))))))

;;;UNIFY from ZM final exam in CS258

(DEFUN UNIFY (X Y)
  (COND ((EQUAL X Y) NIL)
	((ISVAR X) (COND ((OCCUR X Y) 'NO) (T (LIST (CONS X Y))) ))
	((ISVAR Y) (COND ((OCCUR Y X) 'NO) (T (LIST (CONS Y X))) ))
	((OR (ATOM X) (ATOM Y)) 'NO)
	(T ((LAMBDA (S1)
	      (COND ((EQ S1 'NO) 'NO)
		    (T ((LAMBDA (S2) (COND ((EQ S2 'NO) 'NO) (T (COMPOSE S1 S2)) ))
			(UNIFY (SUBLIS S1 (CDR X)) (SUBLIS S1 (CDR Y))))) ))
	    (UNIFY (CAR X) (CAR Y)))) ))


(DEFUN COMPOSE (S1 S2)
  (COND ((NULL S1) S2)
	(T (CONS (CONS (CAAR S1) (SUBLIS S2 (CDAR S1))) (COMPOSE (CDR S1) S2)))))


(DEFUN OCCUR (X Y)
  (OR (EQUAL X Y) (AND (NOT (ATOM Y)) (OR (OCCUR X (CAR Y)) (OCCUR X (CDR Y))))))